COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.ss An Informal Example.
C00006 00003	.ss Fixed points of recursive functions - informal treatment
C00008 ENDMK
C⊗;
.ss An Informal Example.


	If formal proofs of correctness are to be useful, the formalism
must be precise; otherwise the rules will allow proofs of false statements.
In the case of LISP programs, this requires careful attention to
certain details which may make the exposition hard to follow.
Therefore, we begin with an simple example treated informally
which gives some of the ideas that will be treated formally, but if
we were to follow it naively, we could prove false statements.

	Our old friend ⊗append is defined by

	%2u * v ← qif qn u qthen v qelse [qa u].[qd u * v]%1.

We would like to prove it %2associative%1, i.e.
for any lists ⊗u, ⊗v, and ⊗w, we want to prove that

	%2u * [v * w] = [u * v] * w.

	The general idea of the proof is first to prove the proposition
for %2u_=_NIL%1, and then show that if it is true for %2qd u%1, it will
be true for ⊗u.  Having done this an induction principle for lists
allows us to conclude that it is true for all lists ⊗u.  The induction
principle may be written

	%2P[NIL] ∧ ∀u:[P[qd u] ⊃ P[u]]  ⊃ ∀u:P[u]%1,

where the variable ⊗u ranges over all lists, i.e. taking repeated %2cdr%1s
must eventually result in qNIL.

	Our first informal step is to regard this recursive function
definition as an equation, writing

A:	%2u * v = qif qn u qthen v qelse [qa u].[qd u * v]%1

This requires a justification which we will not stop to give.

	For %2u = NIL%1, the desired equation is

	%2qNIL * [v * w] = [qNIL * v] * w%1,

and this easily follows from the general lemma %2qNIL * v = v%1,
which is proved by substituting qNIL for ⊗u in A.
Now we prove associativity assuming it for %2qd u%1, i.e. we assume

	%2[qd u] * [v * w] = [[qd u] * v] * w%1.

Before this we need one more lemma, namely

B:	%2[x . v] * w = x . [v * w]%1.

This is just a calculation using A.  Namely,

	%2[x . v] * w = qif qn [x . v] qthen w qelse qa [x . v] . [qd [x . v] * w]

			= qa [x . v] . [qd [x . v] * w]

			= x . [v * w]%2,

which was to be proved.

	The main result is again obtained by a calculation, namely

	%2[u * v] * w = [qif qn u qthen v qelse qa u .[qd u * v]] * w

			= [qa u . [qd u * v]] * w

			= qa u . [[qd u * v] * w]

			= qa u . [qd u * [v * w]]

			= [qa u . qd u] * [v * w]]

			= u * [v * w]%1,

which proves the theorem from the induction hypothesis.  Applying the
induction principle for lists yields the theorem unconditionally.

	
.ss Fixed points of recursive functions - informal treatment


	In the previous section we replaced the recursive definition
of ⊗append by an equation.  We want to justify this, but the naive
replacement of recursive definitions by equations is wrong.  Consider
the definition

	%2foo x ← A . [foo x]%1.

The equation

	%2foo x = A . [foo x]%1

is certainly wrong, because A.x is different from ⊗x for any S-expression
⊗x.  Since this fact can be proved, the resulting contradiction would
enable us to prove anything, which would scarcely engender user confidence
in programs that were claimed to be proved correct.  One might suppose that
the above is a pathological example, and we could make a rule to exclude
it.  Unfortunately, there is no rule that will exclude all the definitions
that lead to contradiction and admit all the legitimate recursive definitions
that lead to total functions.  Mathematically, this is a consequence of
the fact that the total recursive functions are not a recursively enumerable
set.

	However, it turns out that we can replace recursive definitions
by equations provided we adjoin to the domain of S-expression (or to
any other domain we may be using) an extra element written